#ifndef IC3_H
#define IC3_H

#include "ic3adt.h"

class StrashAIG;  // initialize 
class MinisatIC3; 

typedef MinisatIC3 solver_t; 

struct IC3Param
{
   Minisat::Lit * _lits;        ///< [0-ns) state var , [ns,ns*2) next state var , [ns+ns] next state property
   Minisat::Lit * _rlits;       ///< reverse mapping ( next state literal -> state number )
   unsigned       _nstates;     ///< state umber 
   unsigned       _nvar;        ///< number of variable 
};

class MinisatIC3 : IC3Param , public Minisat::Solver 
{
   unsigned     _uctrl;
   void         recycle();
   Minisat::Lit get_ctrl();

   public:
   
   MinisatIC3( vec< Clause > & c , IC3Param & p );

   void subclause_inductive_relative( const State s ,Clause & c ); ///< use UNSAT witness to extract sub-clause
   bool sat();                   ///< perform F & T & ~P
   bool sat( const Clause & c);  ///< perform F & T & ~c'
   bool sat( const State s );    ///< perform F & T & ~s & s' ( control literal apply and recycle )
   void witness( State s );      ///< 

   private:

   bool MIC( Clause & c );
   bool DOWN( Clause & c );
   void UP( Clause & c );
   bool consecution( Clause & c );
   bool implicate( Clause & c , Clause & c0 , uint8_t * );
   void min( Clause & s , Minisat::Lit ctrl );
   void min_opt( Clause & a , Minisat::Lit ctrl );
   void min_opt_rec( Clause & a , Clause & sup , Minisat::Lit ctrl );
};

class IC3 : StateAllocator , IC3Param , public ClauseKeaper
{
   vec< Clause >    Finit; ///< initial Clause of the solver
   vec< solver_t * > F;     ///< 

   bool strengthen( int k );
   void propagateClause( int k );
   int  inductivelyGeneralize( State s , int min , int k );
   void generateClause( State s , int i , int k );
   bool pushGeneralization( States & set , int k );
   inline MinisatIC3 * addFrame(){ MinisatIC3 * f = new MinisatIC3( Finit , *this); F.push( f ); _clauses.push(); return f; }

   bool addClause( unsigned i , unsigned j , const Clause * c );// from i to j 
   public:
   ~IC3();
   bool init( StrashAIG & aig );///< transform ckt to P and T
   bool prove();
   void ic3info();

   private:
   // much of assertions 
   MinisatIC3 * createSolver( unsigned k );
   bool isInductiveInvariant( unsigned i , State s );
   bool isInductiveInvariant( unsigned i , const Clause & c );
   bool check_sat( unsigned i , State s );
   bool check_ic3_A();
   bool check_ic3_A1();
   bool check_ic3_A4();
   bool check_ic3_Fi_imply_Fi_1( unsigned i );
   bool my_check();
};

#endif
